Skip to content

fix(ci): align the Idris2 version assert with the pinned image (0.8.0) - #31

Merged
hyperpolymath merged 1 commit into
mainfrom
fix/idris2-version-0-8-0
Jul 27, 2026
Merged

fix(ci): align the Idris2 version assert with the pinned image (0.8.0)#31
hyperpolymath merged 1 commit into
mainfrom
fix/idris2-version-0-8-0

Conversation

@hyperpolymath

Copy link
Copy Markdown
Owner

Now that #30 made the assert diagnosable, the real mismatch is visible:

idris2 --version -> Idris 2, version 0.8.0-6ca00e72e
::error::expected Idris 2 0.7.0

The digest-pinned idris2-pack image ships 0.8.0, so the 0.7.0 assertion
could never have matched — CI / required has never passed on its own terms.
This is the last red check on main.

Which side is wrong?

Nothing in the repository actually requires 0.7.0:

  • abi.ipkg declares no version constraint — it depends only on base.
  • The idris2 0.7.0 line in .tool-versions is commented out, so it pins nothing.
  • The only 0.7.0 references were the workflow asserts and their comments.

So "0.7.0" was stale documentation that drifted from the digest. The immutable
digest is the authority
, and the version notes are brought into step with it
rather than the reverse. The typecheck now actually runs against the toolchain
that is genuinely installed.

Also fixes the identical brittle assert in release.yml, which piped
idris2 --version into grep -Fx under pipefail exactly as ci.yml did — it
would have failed the same way, silently, on the next release.

If 0.7.0 was intended

Then the fix is the other direction: re-pin the container to a 0.7.0 image digest.
Say so and I will swap it — but the current pair is contradictory either way.

🤖 Generated with Claude Code

With the assert made diagnosable, the actual mismatch is visible:

    idris2 --version -> Idris 2, version 0.8.0-6ca00e72e
    ::error::expected Idris 2 0.7.0

The digest-pinned idris2-pack image ships 0.8.0, so the 0.7.0 assertion could
never have matched and this job has never passed on its own terms.

Nothing in the repository actually requires 0.7.0: abi.ipkg declares no version
constraint (it depends only on `base`), and the `idris2 0.7.0` line in
.tool-versions is commented out, so it pins nothing. The only 0.7.0 references
were the workflow asserts and their comments — stale documentation that drifted
from the digest.

The immutable digest is the authority, so the version notes are brought into
step with it rather than the other way round. The typecheck now actually runs.

Also fixes the identical brittle assert in release.yml, which piped
`idris2 --version` into `grep -Fx` under pipefail exactly as ci.yml did.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@sonarqubecloud

Copy link
Copy Markdown

@hyperpolymath
hyperpolymath merged commit d29f89e into main Jul 27, 2026
37 of 38 checks passed
@hyperpolymath
hyperpolymath deleted the fix/idris2-version-0-8-0 branch July 27, 2026 13:46
hyperpolymath added a commit that referenced this pull request Jul 27, 2026
…ns (#32)

`CI / required` is the last red check on `main`. After #31 fixed the
version
assert, the job got two steps further and now fails at **Validate
repository
contracts** with exit code 2 and one line of output:

```
jq is required
```

## Root cause

`tests/check-examples.sh:15`:

```bash
command -v jq >/dev/null || { echo "jq is required"; exit 2; }
```

The pinned `idris2-pack` image does not ship `jq`. So the **Trope IR
conformance
test — the one asserting every example lowers to valid Trope IR — has
never
actually executed in CI.** It bailed before testing anything.

That makes this more than a build fix: it turns a step that always died
early
into one that genuinely exercises the language's core guarantee.

## Fix

Same class of problem as the missing `xz` in #28, so the step now
handles both:
collect what is absent, install in a single `apt-get` pass, print both
versions
so the log records what ran. A no-op on images that already have them.

## Verified locally against `origin/main` (d29f89e)

```
bash -n over tests/ scripts/ ............... all parse
tests/check-examples.sh .................... exit 0  → "examples: all lower to valid Trope IR"
tests/aspect_tests.sh ...................... exit 0  → PASS=3 FAIL=0 WARN=0
scripts/check-root-shape.sh ................ exit 0  → 45 entries, 46 permitted
tests/workflows/validate_workflows_test.sh . exit 0  → Workflow validation PASSED
```

Note `check-examples.sh` skips the verdict round-trip when no sibling
`tropecheck` binary is built — that part still needs `trope-checker`,
and is
reported as a `note`, not a pass.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant